b:, f:(b). (n:b. f(n))  {f(mu(f)) & (i:b. i<mu(f)  f(i))} 

latex

Definitions	T, True, Dec(P), P  Q, SQType(T), Unit, P  Q, b, Prop, mu(f), i  j < k, P & Q, AB, ij, , A, False, P  Q, b, {i..j}, x:A. B(x), t  T, , {T}, x:A. B(x)
Lemmas	bool wf, int seg wf, assert wf, nat wf, nat properties, ge wf, mu wf, not wf, bnot wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, decidable int equal, le wf, true wf, squash wf, mu-bound